00010	L(X1 X2) →LE(X1 X2);
00020	(LE(X1 X2) ∧LE(X2 X3)) →LE(X1 X3);
00035	(LE(X1 X2)∧LE(X2 X1))→E(X1 X2);
00050	(L(X1 X2) ∧ L(X2 X3)) →L(X1 X3);
00060	LE(X1 X2) →(E(X1 X2) ∨ L(X1 X2));
00080	;
00100	E(X1 X1); LE(X1 X1);
00200	
00300	LE(M F); LE(F N); LE(L P); LE(P F); LE(F Q); LE(Q CN);
00400	¬L(X1 X1); 
00500	(LE(L X1) ∧L(X1 M) ∧ LE(M X2) ∧ LE(X2 CN))→LE(A(X1) A(X2));
00600	(LE(L X1) ∧ LE(X1 N) ∧ L(N X2) ∧ LE(X2 CN)) → LE(A(X1) A(X2));
00700	¬L(M N);
00800	;
00900	LE(A(F)A(Q)); ;
01000